Nuprl Lemma : component-compatible_wf 11,40
ds:(IdType{i}), da:(IdKndType{i}), A, B:Type{i}, Ca:component{i:l}(ds; da; A; Top),
Cb:component{i:l}
Cb:component(ds; da; B; Top).
component-compatible{i:l}(ds; da; A; B; Ca; Cb)  {i'} 
latex

Definitionsx. t(x), component-compatible(ds;da;T1;T2;C1;C2), , t  T, x:A. B(x), x(s), Component(ds;da;A;B)
LemmasKnd wf, Id wf, component wf, top wf, RealizerScheme wf, pi1 wf, scheme-compatible wf, interface wf

origin